A, B:Type.
AtomFree(Type;A)
 AtomFree(Type;B)
 (eq:EqDecider(A).
 (AtomFree(EqDecider(A);eq)
 ( (f:a:A fp B.
 ( ((a:A. AtomFree(A;a))
 ( ( adom(f). x=f(a)   AtomFree(B;x)
 ( ( AtomFree(a:A fp B;f))) 

latex

Definitions

b, f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), a:A fp B(a), x:AB(x), Type, t  T, x:A. B(x), AtomFree(T;x), EqDecider(T), x. t(x), x:AB(x), Prop, x.A(x), Top, {x:A| B(x) }, x,y. t(x;y), P  Q, type List, nil, (x  l), f(a), deq-member(eq;x;L), x:A. B(x), <a,b>, s = t, A/x,y. B(x;y), 1of(t), eqof(d), p  q, reduce(f;k;as), tl(l), n-m, if a<b c ; d fi, i<j, b, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), Y, ||as||, a<b, A, AB, , , Unit, left+right, , False, P & Q, P  Q, {T}, car.cdr, P  Q, P  Q, 2of(t), S  T, S  T

Lemmas

not functionality wrt iff, deq property, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, ifthenelse wf, eqof wf, cons member, assert-deq-member, nil member, deq-member wf, l member wf, fpf-all wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, deq wf, atom-free wf